ds:fpf(Id; x.Type), k:Knd, x:Id, n:, f:top.
update-spec-decl(update-spec1(k; x; n; s,v.f(s,v)); ds)  (fpf-dom(id-deq; x; ds)) 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), fpf(A; a.B(a)), Knd, , top, x.A(x), P  Q, False, A, A  B, , {x:A| B(x)} , x:AB(x), id-deq, fpf-dom(eq; x; f), b, s = t, prop{i:l}, P  Q, P  Q, P  Q, type List, [], cons(car; cdr), (x  l), x:A  B(x), guard(T), update-spec-vars(upd), update-spec-decl(upd; ds), update-spec1(k; x; n; s,v.f(s;v)), sq_type(T), sqequal(s; t), atom{$n:n}
Lemmas	Id sq, iff functionality wrt iff, all functionality wrt iff, implies functionality wrt iff, member singleton, iff wf, l member wf, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, top wf, nat wf, Knd wf, fpf wf, Id wf